es:ES, A, T:Type, X:AbsInterface(A), base:T, f:(TAT), e:E.
prior-state(f;base;X;e)
=
if e  prior(X) then local-state(f;base;X;prior(X)(e)) else base fi 
 T 

latex

Definitions

(e <loc e'), A c B, local-state(f;base;X;e), , p q, p  q, p  q, e = e', deq-member(eq;x;L), a = b, a = b, qeq(r;s), q_less(a;b), q_le(r;s), eq_atom$n(x;y), [d], a < b, x f y, a < b, null(as), x =a y, (i = j), i z j, i <z j, p =b q, constant_function(f;A;B), r  s, e < e', val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), , , Msg(M), kindcase(k; a.f(a); l,t.g(l;t) ), x,y. t(x;y), x. t(x), Knd, EState(T), EOrderAxioms(E; pred?; info), Id, IdLnk, Unit, EqDecider(T), E(X), f(x)?z, type List, P  Q, P & Q, P  Q, {x:A| B(x)} , Top, x:A.B(x), tt, b, , , ff, False, Void, case b of inl(x) => s(x) | inr(y) => t(y), t.1, let x,y = A in B(x;y), left + right, X(e), x  dom(f), e  X, prior(X), A, b, f(a), P  Q, strong-subtype(A;B), <a, b>, prior-state(f;base;X;e), if b then t else f fi , a:A fp B(a), x:A  B(x), E, AbsInterface(A), Type, ES, x:A. B(x), x:AB(x), t  T, s = t

Lemmas

event system wf, es-interface wf, es-E wf, ifthenelse wf, es-local-prior-state wf, assert wf, not wf, bnot wf, bool wf, subtype rel wf, top wf, es-interface-subtype rel, member wf, es-E-interface-subtype rel, deq wf, unit wf, IdLnk wf, Id wf, EOrderAxioms wf, EState wf, Knd wf, kindcase wf, Msg wf, nat wf, rationals wf, val-axiom wf, cless wf, qle wf, constant function wf, es-E-interface wf, es-prior-interface wf, es-interface-val wf, es-interface-val wf2, es-is-interface wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, es-prior-interface-val